Thanks for creating this PR! I think the definitions provided by this PR fill an important hole in the Coq standard library.

I needed a library for fixed sized integers in the context of the Islaris project and since there is currently no implementation in the standard library, I had to implement my own library (which now lives in std++). I am not the only one who has this problem, as I know of quite a few (at least 5 I think) implementations of fixed size integers libraries. However, it is not really possible to reuse code outside of the standard library since e.g. libraries like std++ cannot have dependencies except Coq. So I think it would be really great to have these core concepts like fixed-size integers provided by the Coq standard library such that they can be shared and built-upon by the ecosystem.

This is not ready for merge-review, but what is already here is representative of what I am proposing. I would appreciate high-level feedback about scope and strategy. For example, it would be neat if another maintainer of (of stdlib, numbers, or even another word/ZnZ library) took a look at every file, module, or **-section and shared their impressions.

Like @MackieLoeffel I also think this fills an important gap in the standard library; projects that want to reason about fixed-size integers, e.g. for proofs about virtually any programming language, currently use a smattering of mostly homegrown implementations. For cryptography proofs, the basic modular arithmetic lemmas and the proof of Fermat's Little Theorem (often used for computing the inverse of a finite field element) are especially useful. I looked through all the code and the setup/design makes sense to me as a heavy user of modular arithmetic in Coq, for whatever that's worth 🙂 I can leave a detailed review if it helps the PR not fall through the cracks, but I'm not a stdlib maintainer.

@coq/number-maintainers Could I get a review on this? Thanks!

Not a review but only a quick look:

• it mostly looks reasonable and certainly should eventually be merged
• it's large, you might want to cut it in smaller PRs (when that make sense) that would be easier to review
• in terms of code organisation, I'd rather put that either in theories/ZArith or in a new theories/Zmod, it seems Numbers is mostly for abstract things and some mess, let's not increase the entropy there
• apparently some NArith_base would be in order too, could be a good opportunity to clarify this
• currently PArith has no dependencies on ZArith, I'm reluctant to add one, if really needed please make separate directories theories/PArith/PArith_base and theories/PArith/PArith or something like that
• why not have something more abstract in the spirit of Numbers/* for N/nat and Z? (apparently the module types in Numbers could have instances for Z/pZ), that may reduce redundancy in some proofs
• what's the link with Cyclic63? (if any, I mean that's also modular arithmetic although on int63 rather than Z, maybe also a motivation for having more abstract modules?)

Please rebase/squash and ping when you consider it ready for final review/merge

Cc @Villetaneuse who may have an opinion too

Thank you for the feedback. Here are quick responses:

• 👍
• This is already a fraction of the code from the initial draft, and I worry looking at smaller pieces might not guide the overall structure well, but I could split further after the high-level structure is decided.
• Yes, I'd be happy with theories/Zmod
• Yes, I think it would be valuable to use Z to prove lemmas about positive and N. But I worry that doing this in a principled manner would be a long-term project.
• Why would separate directories for PArith with and without Z be more desirable than the file in the current PR?
• The lemmas already treat Zmod abstractly whenever possible, but I think codifying this in the logic would be more trouble than it is worth unless there is an immediate, compelling use case. The previous word library I built did use an abstraction like this, and apparently it put off potential users enough to inspire creation of competing libraries. Given the current difficulties with extending Numbers, I don't blame them. What redundancy are you worried about? Nothing in NZDomain looks useful to me.
• Uint63 does present an isomorphic structure based on primitive implementations and axioms. The central difference is that Uint63 also reimplements a bunch of derived operations such as gcd and sqrt for efficiency, whereas the approach I am following in Zmod is to rely on Z whenever possible. I think a valuable future direction would be to ground that specification in Zmod instead of Cyclic (and to move Cyclic to bignums). IMO the right way to do that would be to give a minimal set of lemmas and a tactic that translates goals to Zmod (like zify), without duplicating the Zmod theory for uing63 specifically (as it is for PeanoNat). But I don't want to block Zmod on that refactor and associated compat work.

* This is already a fraction of the code from the initial draft, and I worry looking at smaller pieces might not guide the overall structure well, but I could split further after the high-level structure is decided.

Ok, let's keep it as it is. Please just make sure when rebasing to have clear and consistent commits.

* Yes, I'd be happy with theories/Zmod

Ok

* Yes, I think it would be valuable to use Z to prove lemmas about positive and N. But I worry that doing this in a principled manner would be a long-term project.

Ok for clarifying Narith_base later.

* Why would separate directories for PArith with and without Z be more desirable than the file in the current PR?

Some users want to use PArith without having to depend on the whole ZArith and micromega. As already discussed on zulip, the fact that all those dependencies are not very clear, and not enforced in the CI, led to the current mess. We could hope to clarify this, enabling a clean split into meaningful subpackages, and enforcement of their dependencies in the CI. If only due to the way Coq works (-R and -Q options), having a clean directory tree can only help. I agree the current situation is less than ideal, let's just not make it worse.
To make things clear: I'm strongly opposed to merge anything adding that kind of new dependencies the way it's currently made in this PR.

* The lemmas already treat Zmod abstractly whenever possible, but I think codifying this in the logic would be more trouble than it is worth

Ok, maybe we should indeed accept that modules are not so convenient as an abstraction facility.

* I think a valuable future direction would be to ground that specification in Zmod instead of Cyclic (and to move Cyclic to bignums).

Ok, that was just a question out of curiosity, let's keep things as they are in this PR. And also ok for moving cyclic to bignums in separate PRs (one to bignums for the addition, one here for the deletion).

Some users want to use PArith without having to depend on the whole ZArith and micromega. As already discussed on zulip, the fact that all those dependencies are not very clear, and not enforced in the CI, led to the current mess. We could hope to clarify this, enabling a clean split into meaningful subpackages, and enforcement of their dependencies in the CI. If only due to the way Coq works (-R and -Q options), having a clean directory tree can only help. I agree the current situation is less than ideal, let's just not make it worse.
To make things clear: I'm strongly opposed to merge anything adding that kind of new dependencies the way it's currently made in this PR.

I am struggling to make sense of this requirement. Do you actually intend to require that any lemmas about positive (that would live in Pos.) must be proven without relying on Z and lia? Or is PArith special for some reason, and adding the same lemmas under another path would be acceptable? (Which path?) And why do you want to break up stdlib anyway?

EDIT: As a user, I Require Import ZArith to get all stdlib lemmas about Z, and I would expect the same for PArith and positive though I rarely use it. It would be unexpected if some additional lemmas about Z were present but not made available through ZArith. This PR actualy adds a lemma like this, Fermat's little theorem proven using Zmod. I think this lemma should be made available through a convenience-exports file as well, and ZArith seems like the best candidate. But perhaps what you are getting at is that some users want "the bare minimum to define positive" instead of "everything there is proven about positive", and currently we do not have a stable interface for them. Perhaps we should add one, but I think repurposing PArith to be that interface would be counter to expectations of most users.

Have you considered also looking at CompCert:
https://github.com/AbsInt/CompCert/blob/master/lib/Integers.v

I did look at it a while ago, I just forgot to list it. IIRC the overall conceptual design is rather similar to how what I am doing here applies mod 2^m, but the int interface also includes operations that handle carry flags and sign extension which I am unsure about. I do think it would be valuable to eventually aim for comparable coverage of properties of already included bitwise operations, though.

Is there something specific there that you are interested in?

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

This PR was not rebased after 30 days despite the warning, it is now closed.